/-
Copyright (c) 2023 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen
-/

import ring_theory.dedekind_domain.dvr
import ring_theory.dedekind_domain.ideal

/-!
# Proving a Dedekind domain is a PID

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

This file contains some results that we can use to show all ideals in a Dedekind domain are
principal.

## Main results

 * `ideal.is_principal.of_finite_maximals_of_is_unit`: an invertible ideal in a commutative ring
   with finitely many maximal ideals, is a principal ideal.
 * `is_principal_ideal_ring.of_finite_primes`: if a Dedekind domain has finitely many prime ideals,
   it is a principal ideal domain.
-/

variables {R : Type*} [comm_ring R]

open ideal
open unique_factorization_monoid
open_locale big_operators
open_locale non_zero_divisors

open unique_factorization_monoid

/-- Let `P` be a prime ideal, `x ∈ P \ P²` and `x ∉ Q` for all prime ideals `Q ≠ P`.
Then `P` is generated by `x`. -/
lemma ideal.eq_span_singleton_of_mem_of_not_mem_sq_of_not_mem_prime_ne
  {P : ideal R} (hP : P.is_prime) [is_domain R] [is_dedekind_domain R]
  {x : R} (x_mem : x ∈ P) (hxP2 : x ∉ P^2)
  (hxQ : ∀ (Q : ideal R), is_prime Q → Q ≠ P → x ∉ Q) :
  P = ideal.span {x} :=
begin
  letI := classical.dec_eq (ideal R),
  have hx0 : x ≠ 0,
  { rintro rfl,
    exact hxP2 (zero_mem _) },
  by_cases hP0 : P = ⊥,
  { unfreezingI { subst hP0 },
    simpa using hxP2 },
  have hspan0 : span ({x} : set R) ≠ ⊥ := mt ideal.span_singleton_eq_bot.mp hx0,
  have span_le := (ideal.span_singleton_le_iff_mem _).mpr x_mem,
  refine associated_iff_eq.mp
    ((associated_iff_normalized_factors_eq_normalized_factors hP0 hspan0).mpr
      (le_antisymm ((dvd_iff_normalized_factors_le_normalized_factors hP0 hspan0).mp _) _)),
  { rwa [ideal.dvd_iff_le, ideal.span_singleton_le_iff_mem] },
  simp only [normalized_factors_irreducible ((ideal.prime_of_is_prime hP0 hP).irreducible),
      normalize_eq, multiset.le_iff_count, multiset.count_singleton],
  intros Q,
  split_ifs with hQ,
  { unfreezingI { subst hQ },
    refine (ideal.count_normalized_factors_eq _ _).le;
      simp only [ideal.span_singleton_le_iff_mem, pow_one];
      assumption },
  by_cases hQp : is_prime Q,
  { resetI,
    refine (ideal.count_normalized_factors_eq _ _).le;
      simp only [ideal.span_singleton_le_iff_mem, pow_one, pow_zero, one_eq_top, submodule.mem_top],
    exact hxQ _ hQp hQ },
  { exact (multiset.count_eq_zero.mpr (λ hQi, hQp (is_prime_of_prime (irreducible_iff_prime.mp
      (irreducible_of_normalized_factor _ hQi))))).le }
end

lemma fractional_ideal.is_principal_of_unit_of_comap_mul_span_singleton_eq_top
  {R A : Type*} [comm_ring R] [comm_ring A] [algebra R A] {S : submonoid R} [is_localization S A]
  (I : (fractional_ideal S A)ˣ) {v : A} (hv : v ∈ (↑I⁻¹ : fractional_ideal S A))
  (h : submodule.comap (algebra.linear_map R A) (I * submodule.span R {v}) = ⊤) :
  submodule.is_principal (I : submodule R A) :=
begin
  have hinv := I.mul_inv,
  set J := submodule.comap (algebra.linear_map R A) (I * submodule.span R {v}),
  have hJ : is_localization.coe_submodule A J = I * submodule.span R {v},
  { rw [subtype.ext_iff, fractional_ideal.coe_mul, fractional_ideal.coe_one] at hinv,
    apply submodule.map_comap_eq_self,
    rw [← submodule.one_eq_range, ← hinv],
    exact submodule.mul_le_mul_right ((submodule.span_singleton_le_iff_mem _ _).2 hv) },
  have : (1 : A) ∈ ↑I * submodule.span R {v},
  { rw [← hJ, h, is_localization.coe_submodule_top, submodule.mem_one],
    exact ⟨1, (algebra_map R _).map_one⟩ },
  obtain ⟨w, hw, hvw⟩ := submodule.mem_mul_span_singleton.1 this,
  refine ⟨⟨w, _⟩⟩,
  rw [← fractional_ideal.coe_span_singleton S, ← inv_inv I, eq_comm, coe_coe],
  refine congr_arg coe (units.eq_inv_of_mul_eq_one_left (le_antisymm _ _)),
  { apply_instance },
  { conv_rhs { rw [← hinv, mul_comm] },
    apply fractional_ideal.mul_le_mul_left (fractional_ideal.span_singleton_le_iff_mem.mpr hw) },
  { rw [fractional_ideal.one_le, ← hvw, mul_comm],
    exact fractional_ideal.mul_mem_mul hv (fractional_ideal.mem_span_singleton_self _ _) }
end

/--
An invertible fractional ideal of a commutative ring with finitely many maximal ideals is principal.

https://math.stackexchange.com/a/95857 -/
theorem fractional_ideal.is_principal.of_finite_maximals_of_inv
  {A : Type*} [comm_ring A] [algebra R A] {S : submonoid R} [is_localization S A]
  (hS : S ≤ R⁰) (hf : {I : ideal R | I.is_maximal}.finite)
  (I I' : fractional_ideal S A) (hinv : I * I' = 1) :
  submodule.is_principal (I : submodule R A) :=
begin
  have hinv' := hinv,
  rw [subtype.ext_iff, fractional_ideal.coe_mul] at hinv,
  let s := hf.to_finset,
  haveI := classical.dec_eq (ideal R),
  have coprime : ∀ (M ∈ s) (M' ∈ s.erase M), M ⊔ M' = ⊤,
  { simp_rw [finset.mem_erase, hf.mem_to_finset],
    rintro M hM M' ⟨hne, hM'⟩,
    exact ideal.is_maximal.coprime_of_ne hM hM' hne.symm },
  have nle : ∀ M ∈ s, ¬ (⨅ M' ∈ s.erase M, M') ≤ M := λ M hM, left_lt_sup.1
    ((hf.mem_to_finset.1 hM).ne_top.lt_top.trans_eq (ideal.sup_infi_eq_top $ coprime M hM).symm),
  have : ∀ M ∈ s, ∃ (a ∈ I) (b ∈ I'), a * b ∉ is_localization.coe_submodule A M,
  { intros M hM, by_contra' h,
    obtain ⟨x, hx, hxM⟩ := set_like.exists_of_lt ((is_localization.coe_submodule_strict_mono
      hS (hf.mem_to_finset.1 hM).ne_top.lt_top).trans_eq hinv.symm),
    refine hxM (submodule.map₂_le.2 _ hx), exact h },
  choose! a ha b hb hm using this,
  choose! u hu hum using λ M hM, set_like.not_le_iff_exists.1 (nle M hM),
  let v := ∑ M in s, u M • b M,
  have hv : v ∈ I' := submodule.sum_mem _ (λ M hM, submodule.smul_mem _ _ $ hb M hM),
  refine fractional_ideal.is_principal_of_unit_of_comap_mul_span_singleton_eq_top
    (units.mk_of_mul_eq_one I I' hinv') hv (of_not_not $ λ h, _),
  obtain ⟨M, hM, hJM⟩ := ideal.exists_le_maximal _ h,
  replace hM := hf.mem_to_finset.2 hM,
  have : ∀ (a ∈ I) (b ∈ I'), ∃ c, algebra_map R _ c = a * b,
  { intros a ha b hb, have hi := hinv.le,
    obtain ⟨c, -, hc⟩ := hi (submodule.mul_mem_mul ha hb),
    exact ⟨c, hc⟩ },
  have hmem: a M * v ∈ is_localization.coe_submodule A M,
  { obtain ⟨c, hc⟩ := this _ (ha M hM) v hv,
    refine is_localization.coe_submodule_mono _ hJM ⟨c, _, hc⟩,
    have := submodule.mul_mem_mul (ha M hM) (submodule.mem_span_singleton_self v),
    rwa ← hc at this },
  simp_rw [finset.mul_sum, mul_smul_comm] at hmem,
  rw [← s.add_sum_erase _ hM, submodule.add_mem_iff_left] at hmem,
  { refine hm M hM _,
    obtain ⟨c, (hc : algebra_map R A c = a M * b M)⟩ := this _ (ha M hM) _ (hb M hM),
    rw ← hc at hmem ⊢,
    rw [algebra.smul_def, ← _root_.map_mul] at hmem,
    obtain ⟨d, hdM, he⟩ := hmem,
    rw is_localization.injective _ hS he at hdM,
    exact submodule.mem_map_of_mem
      (((hf.mem_to_finset.1 hM).is_prime.mem_or_mem hdM).resolve_left $ hum M hM) },
  { refine submodule.sum_mem _ (λ M' hM', _),
    rw finset.mem_erase at hM',
    obtain ⟨c, hc⟩ := this _ (ha M hM) _ (hb M' hM'.2),
    rw [← hc, algebra.smul_def, ← _root_.map_mul],
    specialize hu M' hM'.2,
    simp_rw [ideal.mem_infi, finset.mem_erase] at hu,
    exact submodule.mem_map_of_mem (M.mul_mem_right _ $ hu M ⟨hM'.1.symm, hM⟩) },
end

/-- An invertible ideal in a commutative ring with finitely many maximal ideals is principal.

https://math.stackexchange.com/a/95857 -/
theorem ideal.is_principal.of_finite_maximals_of_is_unit
  (hf : {I : ideal R | I.is_maximal}.finite)
  {I : ideal R} (hI : is_unit (I : fractional_ideal R⁰ (fraction_ring R))) :
  I.is_principal :=
(is_localization.coe_submodule_is_principal _ le_rfl).mp
  (fractional_ideal.is_principal.of_finite_maximals_of_inv le_rfl hf I
    (↑(hI.unit⁻¹) : fractional_ideal R⁰ (fraction_ring R))
    hI.unit.mul_inv)

/-- A Dedekind domain is a PID if its set of primes is finite. -/
theorem is_principal_ideal_ring.of_finite_primes [is_domain R] [is_dedekind_domain R]
  (h : {I : ideal R | I.is_prime}.finite) :
  is_principal_ideal_ring R :=
⟨λ I, begin
  obtain rfl | hI := eq_or_ne I ⊥,
  { exact bot_is_principal },
  apply ideal.is_principal.of_finite_maximals_of_is_unit,
  { apply h.subset, exact @ideal.is_maximal.is_prime _ _ },
  { exact is_unit_of_mul_eq_one _ _ (fractional_ideal.coe_ideal_mul_inv I hI) },
end⟩

variables [is_domain R] [is_dedekind_domain R]
variables (S : Type*) [comm_ring S] [is_domain S]
variables [algebra R S] [module.free R S] [module.finite R S]
variables (p : ideal R) (hp0 : p ≠ ⊥) [is_prime p]
variables {Sₚ : Type*} [comm_ring Sₚ] [algebra S Sₚ]
variables [is_localization (algebra.algebra_map_submonoid S p.prime_compl) Sₚ]
variables [algebra R Sₚ] [is_scalar_tower R S Sₚ]
/- The first hypothesis below follows from properties of the localization but is needed for the
second, so we leave it to the user to provide (automatically). -/
variables [is_domain Sₚ] [is_dedekind_domain Sₚ]

include S hp0

/-- If `p` is a prime in the Dedekind domain `R`, `S` an extension of `R` and `Sₚ` the localization
of `S` at `p`, then all primes in `Sₚ` are factors of the image of `p` in `Sₚ`. -/
lemma is_localization.over_prime.mem_normalized_factors_of_is_prime [decidable_eq (ideal Sₚ)]
  {P : ideal Sₚ} (hP : is_prime P) (hP0 : P ≠ ⊥) :
  P ∈ normalized_factors (ideal.map (algebra_map R Sₚ) p) :=
begin
  have non_zero_div : algebra.algebra_map_submonoid S p.prime_compl ≤ S⁰ :=
    map_le_non_zero_divisors_of_injective _ (no_zero_smul_divisors.algebra_map_injective _ _)
      p.prime_compl_le_non_zero_divisors,
  letI : algebra (localization.at_prime p) Sₚ := localization_algebra p.prime_compl S,
  haveI : is_scalar_tower R (localization.at_prime p) Sₚ := is_scalar_tower.of_algebra_map_eq
    (λ x, by erw [is_localization.map_eq, is_scalar_tower.algebra_map_apply R S]),
  obtain ⟨pid, p', ⟨hp'0, hp'p⟩, hpu⟩ :=
    (discrete_valuation_ring.iff_pid_with_one_nonzero_prime (localization.at_prime p)).mp
      (is_localization.at_prime.discrete_valuation_ring_of_dedekind_domain R hp0 _),
  have : local_ring.maximal_ideal (localization.at_prime p) ≠ ⊥,
  { rw submodule.ne_bot_iff at ⊢ hp0,
    obtain ⟨x, x_mem, x_ne⟩ := hp0,
    exact ⟨algebra_map _ _ x,
      (is_localization.at_prime.to_map_mem_maximal_iff _ _ _).mpr x_mem,
      is_localization.to_map_ne_zero_of_mem_non_zero_divisors _ p.prime_compl_le_non_zero_divisors
        (mem_non_zero_divisors_of_ne_zero x_ne)⟩ },
  rw [← multiset.singleton_le, ← normalize_eq P,
      ← normalized_factors_irreducible (ideal.prime_of_is_prime hP0 hP).irreducible,
      ← dvd_iff_normalized_factors_le_normalized_factors hP0, dvd_iff_le,
      is_scalar_tower.algebra_map_eq R (localization.at_prime p) Sₚ, ← ideal.map_map,
      localization.at_prime.map_eq_maximal_ideal, ideal.map_le_iff_le_comap,
      hpu (local_ring.maximal_ideal _) ⟨this, _⟩, hpu (comap _ _) ⟨_, _⟩],
  { exact le_rfl },
  { have hRS : algebra.is_integral R S := is_integral_of_noetherian
      (is_noetherian_of_fg_of_noetherian' module.finite.out),
    exact mt (ideal.eq_bot_of_comap_eq_bot (is_integral_localization hRS)) hP0 },
  { exact ideal.comap_is_prime (algebra_map (localization.at_prime p) Sₚ) P },
  { exact (local_ring.maximal_ideal.is_maximal _).is_prime },
  { rw [ne.def, zero_eq_bot, ideal.map_eq_bot_iff_of_injective],
    { assumption },
    rw is_scalar_tower.algebra_map_eq R S Sₚ,
    exact (is_localization.injective Sₚ non_zero_div).comp
      (no_zero_smul_divisors.algebra_map_injective _ _) },
end

/-- Let `p` be a prime in the Dedekind domain `R` and `S` be an integral extension of `R`,
then the localization `Sₚ` of `S` at `p` is a PID. -/
theorem is_dedekind_domain.is_principal_ideal_ring_localization_over_prime :
  is_principal_ideal_ring Sₚ :=
begin
  letI := classical.dec_eq (ideal Sₚ),
  letI := classical.dec_pred (λ (P : ideal Sₚ), P.is_prime),
  refine is_principal_ideal_ring.of_finite_primes
    (set.finite.of_finset (finset.filter (λ P, P.is_prime)
      ({⊥} ∪ (normalized_factors (ideal.map (algebra_map R Sₚ) p)).to_finset))
      (λ P, _)),
  rw [finset.mem_filter, finset.mem_union, finset.mem_singleton, set.mem_set_of,
      multiset.mem_to_finset],
  exact and_iff_right_of_imp (λ hP, or_iff_not_imp_left.mpr
    (is_localization.over_prime.mem_normalized_factors_of_is_prime S p hp0 hP))
end
